翻訳と辞書 Words near each other ・ System utility ・ System utility (system engineering) ・ System V Interface Definition ・ System V printing system ・ System deployment ・ System Deployment Image ・ System Design and Management (MIT) ・ System Design Review ・ System Development Corporation ・ System distribution ・ System Divide ・ System dynamics ・ System Dynamics Society ・ System equivalence ・ System Express ・ System F ・ System F-sub ・ System Fault Tolerance ・ System file ・ System File Checker ・ System Flaw ・ System Floors (UK) Ltd v Daniel ・ System folder ・ System for Award Management ・ System for Cross-domain Identity Management ・ System for Electronic Document Analysis and Retrieval ・ System for Information on Grey Literature in Europe ・ System for Teaching Experimental Psychology ・ System G ・ System G (supercomputer) Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク System F ： ウィキペディア英語版 System F System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974). Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally has variables ranging over ''types'', and binders for them. As an example, the fact that the identity function can have any type of the form A→ A would be formalized in System F as the judgment :$\backslash vdash\; \backslash Lambda\backslash alpha.\; \backslash lambda\; x^\backslash alpha.x:\; \backslash forall\backslash alpha.\backslash alpha\; \backslash to\; \backslash alpha$ where $\backslash alpha$ is a type variable. The upper-case $\backslash Lambda$ is traditionally used to denote type-level functions, as opposed to the lower-case $\backslash lambda$ which is used for value-level functions. (The superscripted $\backslash alpha$ means that the bound ''x'' is of type $\backslash alpha$; the expression after the colon is the type of the lambda expression preceding it.) As a term rewriting system, System F is strongly normalizing. However, type inference in System F (without explicit type annotations) is undecidable. Under the Curry–Howard isomorphism, System F corresponds to the fragment of second-order intuitionistic logic that uses only universal quantification. System F can be seen as part of the lambda cube, together with even more expressive typed lambda calculi, including those with dependent types. == Logic and predicates == The $\backslash scriptstyle\; \backslash mathsf$ type is defined as: $\backslash scriptstyle\backslash forall\backslash alpha.\backslash alpha\; \backslash to\; \backslash alpha\; \backslash to\; \backslash alpha$, where $\backslash scriptstyle\backslash alpha$ is a type variable. This means: $\backslash scriptstyle\; \backslash mathsf$ is the type of all functions which take as input a type α and two expressions of type α, and produce as output an expression of type α (note that we consider $\backslash to$ to be right-associative.) The following two definitions for the boolean values $\backslash scriptstyle\backslash mathbf$ and $\backslash scriptstyle\backslash mathbf$ are used, extending the definition of Church booleans: : $\backslash mathbf\; =\; \backslash Lambda\backslash alpha\backslash lambda\; x^\; \backslash lambda\; y^\backslash alphax$ 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.